| Definitions | Dsys, t  T, Unit, Type, IdLnk, left + right, Id,  , x:A  B(x),  x:A. B(x), M(i), M.(timed)state, Void, ma-prob(M;b), Outcome, b dom(M.prob), if b then t else f fi , M.state,  , Feasible(D), d-comp-partial-world(D; v; sched; dec; discrete; t), queue(l;t), d-world(D;v;sched;dec;discrete), <a, b>, M.dout2(l;tg), Msg(M), type List, s = t, P   Q, False,  A, A  B,  , {x:A| B(x)} , snds(l;t), rcvs(l;t), True,  T, nth_tl(n;as), source(l),  x.A(x), concat(ll), {i..j }, upto(n), #$n, M.dout(l,tg), P & Q, i j < k, w.M, Msg, m(l;t), d-partial-world(D;f;t';s;d), ||as||,  , a < b,  b,  b, l[i], i z j, S  T, i <z j, P  Q, x:A  B(x), P Q, onlnk(l;mss), m(i;t), d-comp(D; v; sched; dec; d), CV(F), f(a), d-world-state(D;i), M.Msg, mlnk(m), a = b, filter(P;l), Msg(da), Action(i), a(i;t), map(f;as), destination(l), M.da(a), w-action-dec(TA;M;i), Action(dec), kind(a), isnull(a), w.TA, isrcv(l;a), ff, lnk(k), locl(a), Knd,  x. t(x), t.1, isrcv(k), d-decl(D;i), null |
| Lemmas | null-action wf, w-a wf, action wf, assert of bnot, not wf, isrcv wf, pi1 wf, Knd wf, w-action-dec wf, ma-da wf, locl wf, lnk wf, bfalse wf, w-action wf, ldst wf, select upto, filter wf, eq lnk wf, mlnk wf, ma-msg wf, mlnk wf d, CV wf, d-world-state wf, d-comp wf2, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, bnot of lt int, assert of le int, lt int wf, le int wf, select wf, assert wf, bnot wf, length wf1, length upto, d-comp-partial-world wf, w-ml wf, le wf, subtype rel list, w-Msg wf, d-world wf, subtype rel self, ma-dout wf, upto wf, int seg wf, map equal, concat wf, Msg wf, ma-dout2 wf, lsrc wf, nth tl wf, squash wf, true wf, d-feasible wf, bool wf, ma-st wf, ifthenelse wf, ma-prob-dom wf, p-outcome wf, ma-prob wf, ma-tst wf, d-m wf, Id wf, nat wf, IdLnk wf, unit wf, dsys wf |
dec:(i,a:Id